A:Type, eq:EqDecider(A), B:(AType), f:a:A fp B(a), P:(A).
(a:A. Dec(P(a)))
 (fp,fnp:a:A fp B(a)
 ((f  fp  fnp & fp  fnp  f
 (& (a:A. (a  dom(fp))  P(a)) & (a:A. (a  dom(fnp))  (P(a)))
 (& fpf-domain(fp)  fpf-domain(f)
 (& fpf-domain(fnp)  fpf-domain(f))) 

latex

Definitions

x:A  B(x), a:A fp B(a), Type, t  T, x:A. B(x), EqDecider(T), x:AB(x), f(a), x(s), x. t(x), , Dec(P), f  g, P & Q, b, Void, L1  L2, x:A. B(x), P  Q, False, A, <a, b>, (x  l), {x:A| B(x)} , [d], x.A(x), filter(P;l), type List, s = t, a < b, #$n, ||as||, A  B, , , l[i], A c B, S  T, suptype(S; T), P  Q, b, Top, fpf-domain(f), x  dom(f), f  g, f(x), f(x)?z, deq-member(eq;x;L), if b then t else f fi , as @ bs, P  Q, {T}, P  Q, left + right, , Unit

Lemmas

filter is sublist, eqtt to assert, eqff to assert, bool wf, member append, or functionality wrt iff, iff transitivity, assert of bnot, not functionality wrt iff, and functionality wrt iff, dcdr-to-bool-equivalence, assert-deq-member, append wf, deq-member wf, fpf-join wf, fpf-sub wf, assert wf, fpf-dom wf, not wf, sublist wf, fpf-domain wf, fpf-trivial-subtype-top, bnot wf, member filter, filter wf, dcdr-to-bool wf, subtype rel dep function, subtype rel set, nat wf, length wf1, select wf, l member subtype, l member wf, decidable wf, fpf wf, deq wf